$\forall$$T$:Type, $m$, $n$:$\mathbb{Z}$, $f$:(\{$m$..$n$$^{-}$\}$\rightarrow$$T$). $n$$<$$m$ $\vee$ $\parallel$$f$\{$m$..$n$$^{-}$\}$\parallel$ $=$ $n$$-$$m$